Global Definition

Model Name

First of all, you can give a name for your model using the following syntax in the first line of your model. The model name is used internally as an ID for simulator to find the correct drawing pictures, if any. It is optional.

//@@Model Name@@

Constants

A global constant is defined using the following syntax,

#define max 5;

#define is a keyword used for multiple purposes. Here it defines a global constant named max, which has the value 5. The semi-colon marks the end of the 'sentence'.

Note: the constant value can only be integer value (both positive and negative) and Boolean value (true or false).

Constant enumeration can be defined using keyword enum. For example, enum {red, blue, green}; is the syntactic sugar for the following:

• #define red 0;
• #define blue 1;
• #define green 2;

Variables/arrays

A global variable is defined using the following syntax,

var knight = 0;

where var is a key word for defining a variable and knight is the variable name. Initially, knight has the value 0. Semi-colon is used to mark the end of the 'sentence' as above. We remark the input language of PAT is weakly typed and therefore no typing information is required when declaring a variable. Cast between incompatible types may result in a run-time exception. A fixed-size array may be defined as follows,

var board = [3, 5, 6, 0, 2, 7, 8, 4, 1];

where board is the array name and its initial value is specified as the sequence, e.g., board[0] = 3. The following defines an array of size 3.

var leader[3];

All elements in the array are initialized to be 0.

Note for multi-dimensional array: PAT supports multi-dimensional arrays by converting them into one dimensional array. You can declare and use multi-dimensional arrays as follows. The only restriction is that you cannot assign multi-dimensional array constant to multi-dimensional arrays variables. To initialize a multi-dimensional array, you need to do it explicitly in some events.

• var matrix[3*N][10];
• var matrix[1][6] = 3;

Variable range specification: users can provide the range of the variables/arrays explicitly by giving lower bound or upper bound or both. In this way, the model checkers and simulator can report the out-of-range violation of the variable values to help users to monitor the variable values. The syntax of specifying range values are demonstrated as follows.

• var knight : {0..} = 0;
• var board : {0..10} = [3, 5, 6, 0, 2, 7, 8, 4, 1];
• var leader[N] : {..N-1}; //where N is a constant defined.

Array Initialization: To ease the modeling, PAT supports fast array initialization using following syntax.

• #define N 2;
• var array = [1(2), 3..6, 7(N*2), 12..10];
• //the above is same as the following
• var array = [1, 1, 3, 4, 5, 6, 7, 7, 7, 7, 12, 11, 10];

In the above syntax, 1(2) and 7(N*2) allow user to quickly create an array with same initial values. 3..6 and 12..10 allow user to write quick increasing and decreasing loop to initialize the array.

User defined type: To ease the modeling, PAT allows users to define any data structures and use them in PAT models. The following shows the syntax.

• var <Type> x ; //default constructor of Type class will be called.
• var <Type> x = new Type(1, 2); //constructor with two int parameters will be called.

Hidden variable: To simplify the model, PAT introduces the hidden variables which can be used as normal variables. The only difference is that hidden variable is a kind of secondary variable, which is not included in the state details. The idea of secondary is to use redundant .

• var a; var b;
• hvar difference; //secondary variable to store the difference between a and b.

Channels

In TA module, process can synchronize over channel. A normal channel is declared as follows,

channel c ;

where channel  is a key word for declaring channels only, c is the channel name, the buffer size of the channel is 1. 

         channel c[5] ;

where c is an array of channels, with the array size is 5. The concrete channel depends on the current valuation which is the value of the array index.

Propositions

In addition, the key word #define may be used to define propositions. For instance,

#define goal x == 0;

where goal is the name of the proposition and x == 0 is what goal means. A proposition name is used in the same way as global constant is used. For instance, given the above definition, we may write the following,

if (goal) { P } else { Q };

which means if the value of x is 0 then do P else do Q. We remark that propositions are the basic elements of LTL formulae.

Clocks

A clock may be a variable or an array. All the clocks progress synchronously and real-time constraints are captured by explicitly setting/resetting clock variables. A clock may be defined as follows:

• clock x; //clock is a variable.
• clock y[3]; //clock is an array.

System Definition

A system is defined as an equation in the following syntax,

P(x1, x2, ...,xn) = Exp;

where P is the system name, x1, ..., xn is an optional list of system parameters and Exp is a process expression which is a process defined as a timed automaton or the interleaving processes that are defined as timed automata. The process expression determines the computational logic of the system. A system without parameters is written either as P() or P

For example, a system Sys can be defined in such following ways:

• Sys = P; //P is a defined processes without parameters.
• Sys = Q(1); //Q is a defined processes with a parameter.
• Sys = P() ||| Q(0); //Two interleaving processes.

where ||| denotes interleaving. Both P and Q may perform their local actions without referring to each other. Notice that P and Q can still communicate via shared variables or channels. The generalized form of interleaving is written as,

||| x:{0..n} @ P(x);

Assertions

TA module supports all assertions such as deadlock freeness, reachability, the full set of Linear Temporal Logic (LTL) in CSP Module.